Lemma equation_of_function:
  forall (f: Set -> Set) x y,
    (f x) = (f y) -> (f y) = (f x).
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.